\begin{tabbing} ma{-}interface\=\{i:l\}\+ \\[0ex]($T$) \-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$i$:Id fp$\rightarrow$\+ \\[0ex]${\it ds}$:$x$:Id fp$\rightarrow$ Type\{i\} \\[0ex]$\times$ $k$:\{$k$:Knd$\mid$ $\uparrow$hasloc($k$;$i$)\} fp$\rightarrow$ $V$:Type\{i\} $\times$ (State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($T$ + Top)) \- \end{tabbing}